00100	VAR:V;
00200	PRE_OP:C1,C2,C3,C4,C5,C6,C7,C8,C9,C10,C11;
00300	PRE_PRED:P0,P1,P2,P3;
00350	EQUALITY:P0;
00400	CL1:P1(V1,C1,V1);
00500	CL2:P1(C1,V1,V1);
00600	CL3:P1(V1,V2,V3)∧P1(V2,V4,V5)∧P1(V3,V4,V6)⊃P1(V1,V5,V6);
00700	CL4:P1(V1,V2,V3)∧P1(V2,V4,V5)∧P1(V1,V5,V6)⊃P1(V3,V4,V6);
00800	CL5:P1(V1,V1,V2)⊃P1(V1,V2,C1);
00900	CL6:P1(V1,V1,V2)⊃P1(V2,V1,C1);
01000	CL7:P1(V1,V2,V3)∧P1(V1,V2,V4)⊃P0(V3,V4);
01100	CL8:P2(V1,V2,V3)⊃P1(V1,V2,V3);
01200	CL9:P3(V1,V2)⊃P1(V1,V2,C1);
01300	CL10:P3(V1,V2)⊃P1(V2,V1,C1);
01400	CL11:P3(V1,V2)⊃P1(V1,V1,V2);
01500	CL12:P2(C2,C3,C4);
01600	CL13:P2(C2,C2,C5);
01700	CL14:P2(C3,C3,C6);
01800	CL15:P2(C4,C5,C7);
01900	CL16:P2(C7,C6,C8);
02000	CL17:P2(C8,C8,C9);
02100	CL18:P2(C8,C3,C10);
02200	CL19:P2(C10,C9,C11);
02300	THM:P1(C11,C6,C1);
02400	;